package flowlogic;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;

import com.microsoft.z3.Context;
import com.microsoft.z3.Z3Exception;

import ast.DQCSystem;
import ast.Procedure;
import ast.Term;

public class SystemJudgement extends FLJudgement {
	
	private DQCSystem system;
	private HashMap<String, HashSet<Term>> kappa;
	private PsiNode psi;
	
	public SystemJudgement(DQCSystem sys) 
	{
		system = sys;
		setRho(new HashMap<String, HashSet<Term>>());
		kappa = new HashMap<String, HashSet<Term>>();
		psi = new PsiNode();
	}
	
	public HashMap<String, HashSet<Term>> getKappa()
	{
		return kappa;
	}
	
	public PsiNode getPsi()
	{
		return psi;
	}
	
	public String toString()
	{
		return "rho, kappa |- SYS " + psi;
	}
	
	public ArrayList<DischargeResult> discharge() throws Z3Exception 
	{
		ArrayList<DischargeResult> resList = new ArrayList<DischargeResult>();
		Context ctx = FLAnalysis.getCtx();
		
		NetworkJudgement njdgt = new NetworkJudgement(
				system.getNetwork(), getRho(), kappa, ctx.mkTrue());
		resList.add(njdgt);
		resList.add(new Inclusion(njdgt.getPsi(), psi, true));
		
		ArrayList<Procedure> procList = system.getProcedures();
		ProcessJudgement curPjdgt;
		for (Procedure proc : procList) {
			curPjdgt = new ProcessJudgement(
					proc.getProcess(), getRho(), kappa, ctx.mkTrue());
			resList.add(curPjdgt);
			resList.add(new Inclusion(curPjdgt.getPsi(), psi, true));
		}
		
		return resList;
	}

}
